1. Field of the Invention
The present invention relates to techniques for verifying a hardware design to ensure that the design operates correctly. More specifically, the present invention relates to a method and an apparatus for formally proving the functional equivalence of pipelined designs containing memories.
2. Related Art
Advanced Electronic Design Automation (EDA) tools presently make it possible to design extremely complex integrated circuits (ICs). EDA tools typically transform a high-level functional specification of a design into a more detailed register-transfer level (RTL) specification, which is in turn mapped to a set of transistor components and wires in a given fabrication technology. The components and their interconnections then go through a layout phase in which the system attempts to minimize the size of the circuit while also meeting detailed timing and power requirements. Throughout these steps, a set of verification and testing tools attempt to verify that the final result of the design process works and is true to the original functional specification.
While the design process has been automated where possible, some phases of the design effort remain manual. For example, a team of designers typically creates the RTL specification manually based on the system-level specification, and in doing so may introduce errors into the design. Some formal verification tools attempt to find such errors, for instance by proving the formal equivalence of a system-level specification for a design (e.g. written in C++) to the RTL version. However, due to the complexity of modern designs, verifying formal equivalence is a complicated and computationally expensive process. For instance, some pipelined designs may have a different number of stages in the system-level specification than the RTL specification, and may also include memories which can be read to or written from in every pipeline stage. Note that such memories can be large, and that the memory architecture and data layout may vary significantly between the two specifications. In order to determine whether two versions of such a pipelined design are equivalent, the verification tool attempts to prove that the contents of the memories are the same, which involves a prohibitively expensive sequential equivalence check.
Hence, what is needed is a method and an apparatus for verifying the functional equivalence of pipelined designs containing memories without the above-described problems.